Inference at * 
Iof proof for Lemma int le to int upper:


  i:, A:({i...}). {j:. (i  j)  A(j)}  {j:{i...}. A(j)} 

latex

 by ((((((Unfold `guard` 0) 
CollapseTHEN (GenUnivCD))) 
CollapseTHENM (HypBackchain))) 

CoCollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t
C) inil_term))) 

latex

C.

Definitions	False, A, t  T, P  Q, P  Q, x(s), A  B, P  Q, {T}, P  Q, , {i...}, x:A. B(x)
Lemmas	le wf, int upper wf